FDL - Step of Proof: bor-to-and

Step of Proof: bor-to-and

11,40

Inference at *
Iof proof for Lemma bor-to-and:

a, b:

. ((a

b) ~ ff)

{(a ~ ff) & (b ~ ff)}

by ((if (((first_nat 2:n)) = 0) then (Repeat ((D (0)

)

CollapseTHENA (Auto

)

C)) else (RepeatFor (first_nat 2:n) ((D (0)

)

CollapseTHENA (Auto

)

)))

)

CollapseTHEN ((

CUnfold `guard` ( 0)

)

CollapseTHEN ((AutoBoolCase a)

CollapseTHEN (AutoBoolCase b)

)

Definitions SQType(T), {T}, left + right, Unit, P Q, x:A B(x), x:AB(x), , , s = t, b, A, b, x:A. B(x), t T, P Q, s ~ t, P & Q

Lemmas bool wf, bool sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf

Definitions	SQType(T), {T}, left + right, Unit, P Q, x:A B(x), x:AB(x), , , s = t, b, A, b, x:A. B(x), t T, P Q, s ~ t, P & Q
Lemmas	bool wf, bool sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf